Nuprl Definition : chain_config_ind
11,40
postcript
pdf
chain_config_ind(
x
;
head
;
tail
;
id
.
pred
(
id
);
id
,
num
.
succ
(
id
;
num
))
== case
x
==
of inl(
x
) =>
head
== o
| inr(
x
) => case
x
== o| inr(
x
) =>
of inl(
x
) =>
tail
== o| inr(
x
) => o
| inr(
x
) => case
x
of inl(
x
) =>
pred
(
x
) | inr(
x
) =>
succ
(
x
.1;
x
.2)
latex
Definitions
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
t
.1
,
t
.2
FDL editor aliases
chain_config_ind, chain_config_ind
origin